;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Ilist
  (sig occurrences-equal (item lst))
  (sig sumlist (x))
  
  (con rationalp-sumlist
       (implies (rational-listp x)
                (rationalp (sumlist x))))
  
  (con realp-sumlist
       (implies (real-listp x)
                (realp (sumlist x))))

  ;; This is the main lemma.  The sum of a list can be computed by
  ;; splitting the list up into two parts and adding each part separately.
  (con sumlist-append
    (equal (sumlist (append x y))
           (+ (sumlist x) (sumlist y))))

)